(set-logic HORN)
(set-option :fp.engine spacer)
(declare-fun WRAP (Int ) Bool)
(declare-fun NEST (Int ) Bool)
(declare-fun WEEE (Int ) Bool)
(assert (forall ((m Int)) (=> (= m 0) (WRAP m))))
(assert (forall ((m Int)) (=> (WRAP m) (NEST m))))
(assert (forall ((m Int)) (=> (NEST m) (WEEE m))))
(assert (forall ((m Int) (m1 Int)) (=> (and (WEEE m) (= m1 (+ m 1))) (WEEE m1))))
(assert (forall ((m Int)) (=> (WEEE m) (NEST m))))
(assert (forall ((m Int)) (=> (NEST m) (WRAP m))))
(assert (forall ((m Int)) (=> (and (WRAP m) (not (>= m 0))) false)))
(check-sat)